#include <stdint.h>
#include <stdbool.h>
#include <x86intrin.h>
#include "liblow.h"

#include "ladderstep.h"

typedef unsigned int uint128_t __attribute__((mode(TI)));

#if (defined(__GNUC__) || defined(__GNUG__)) && !(defined(__clang__)||defined(__INTEL_COMPILER))
// https://gcc.gnu.org/bugzilla/show_bug.cgi?id=81294
#define _subborrow_u32 __builtin_ia32_sbb_u32
#define _subborrow_u64 __builtin_ia32_sbb_u64
#endif

#undef force_inline
#define force_inline __attribute__((always_inline))

void force_inline ladderstep(uint64_t* out, uint64_t x15, uint64_t x16, uint64_t x14, uint64_t x12, uint64_t x10, uint64_t x25, uint64_t x26, uint64_t x24, uint64_t x22, uint64_t x20, uint64_t x33, uint64_t x34, uint64_t x32, uint64_t x30, uint64_t x28, uint64_t x43, uint64_t x44, uint64_t x42, uint64_t x40, uint64_t x38, uint64_t x51, uint64_t x52, uint64_t x50, uint64_t x48, uint64_t x46)
{  uint64_t x53 = (x25 + x33);
{  uint64_t x54 = (x26 + x34);
{  uint64_t x55 = (x24 + x32);
{  uint64_t x56 = (x22 + x30);
{  uint64_t x57 = (x20 + x28);
{  uint64_t x58 = ((0xffffffffffffe + x25) - x33);
{  uint64_t x59 = ((0xffffffffffffe + x26) - x34);
{  uint64_t x60 = ((0xffffffffffffe + x24) - x32);
{  uint64_t x61 = ((0xffffffffffffe + x22) - x30);
{  uint64_t x62 = ((0xfffffffffffda + x20) - x28);
{  uint64_t x63 = (x43 + x51);
{  uint64_t x64 = (x44 + x52);
{  uint64_t x65 = (x42 + x50);
{  uint64_t x66 = (x40 + x48);
{  uint64_t x67 = (x38 + x46);
{  uint64_t x68 = ((0xffffffffffffe + x43) - x51);
{  uint64_t x69 = ((0xffffffffffffe + x44) - x52);
{  uint64_t x70 = ((0xffffffffffffe + x42) - x50);
{  uint64_t x71 = ((0xffffffffffffe + x40) - x48);
{  uint64_t x72 = ((0xfffffffffffda + x38) - x46);
{  uint128_t x73 = ((uint128_t)x67 * x62);
{  uint128_t x74 = (((uint128_t)x67 * x61) + ((uint128_t)x66 * x62));
{  uint128_t x75 = ((((uint128_t)x67 * x60) + ((uint128_t)x65 * x62)) + ((uint128_t)x66 * x61));
{  uint128_t x76 = (((((uint128_t)x67 * x59) + ((uint128_t)x64 * x62)) + ((uint128_t)x66 * x60)) + ((uint128_t)x65 * x61));
{  uint128_t x77 = ((((((uint128_t)x67 * x58) + ((uint128_t)x63 * x62)) + ((uint128_t)x64 * x61)) + ((uint128_t)x66 * x59)) + ((uint128_t)x65 * x60));
{  uint64_t x78 = (x63 * 0x13);
{  uint64_t x79 = (x66 * 0x13);
{  uint64_t x80 = (x65 * 0x13);
{  uint64_t x81 = (x64 * 0x13);
{  uint128_t x82 = ((((x73 + ((uint128_t)x78 * x61)) + ((uint128_t)x79 * x58)) + ((uint128_t)x80 * x59)) + ((uint128_t)x81 * x60));
{  uint128_t x83 = (((x74 + ((uint128_t)x78 * x60)) + ((uint128_t)x80 * x58)) + ((uint128_t)x81 * x59));
{  uint128_t x84 = ((x75 + ((uint128_t)x78 * x59)) + ((uint128_t)x81 * x58));
{  uint128_t x85 = (x76 + ((uint128_t)x78 * x58));
{  uint64_t x86 = (uint64_t) (x82 >> 0x33);
{  uint64_t x87 = ((uint64_t)x82 & 0x7ffffffffffff);
{  uint128_t x88 = (x86 + x83);
{  uint64_t x89 = (uint64_t) (x88 >> 0x33);
{  uint64_t x90 = ((uint64_t)x88 & 0x7ffffffffffff);
{  uint128_t x91 = (x89 + x84);
{  uint64_t x92 = (uint64_t) (x91 >> 0x33);
{  uint64_t x93 = ((uint64_t)x91 & 0x7ffffffffffff);
{  uint128_t x94 = (x92 + x85);
{  uint64_t x95 = (uint64_t) (x94 >> 0x33);
{  uint64_t x96 = ((uint64_t)x94 & 0x7ffffffffffff);
{  uint128_t x97 = (x95 + x77);
{  uint64_t x98 = (uint64_t) (x97 >> 0x33);
{  uint64_t x99 = ((uint64_t)x97 & 0x7ffffffffffff);
{  uint64_t x100 = (x87 + (0x13 * x98));
{  uint64_t x101 = (x100 >> 0x33);
{  uint64_t x102 = (x100 & 0x7ffffffffffff);
{  uint64_t x103 = (x101 + x90);
{  uint64_t x104 = (x103 >> 0x33);
{  uint64_t x105 = (x103 & 0x7ffffffffffff);
{  uint64_t x106 = (x104 + x93);
{  uint128_t x107 = ((uint128_t)x57 * x72);
{  uint128_t x108 = (((uint128_t)x57 * x71) + ((uint128_t)x56 * x72));
{  uint128_t x109 = ((((uint128_t)x57 * x70) + ((uint128_t)x55 * x72)) + ((uint128_t)x56 * x71));
{  uint128_t x110 = (((((uint128_t)x57 * x69) + ((uint128_t)x54 * x72)) + ((uint128_t)x56 * x70)) + ((uint128_t)x55 * x71));
{  uint128_t x111 = ((((((uint128_t)x57 * x68) + ((uint128_t)x53 * x72)) + ((uint128_t)x54 * x71)) + ((uint128_t)x56 * x69)) + ((uint128_t)x55 * x70));
{  uint64_t x112 = (x53 * 0x13);
{  uint64_t x113 = (x56 * 0x13);
{  uint64_t x114 = (x55 * 0x13);
{  uint64_t x115 = (x54 * 0x13);
{  uint128_t x116 = ((((x107 + ((uint128_t)x112 * x71)) + ((uint128_t)x113 * x68)) + ((uint128_t)x114 * x69)) + ((uint128_t)x115 * x70));
{  uint128_t x117 = (((x108 + ((uint128_t)x112 * x70)) + ((uint128_t)x114 * x68)) + ((uint128_t)x115 * x69));
{  uint128_t x118 = ((x109 + ((uint128_t)x112 * x69)) + ((uint128_t)x115 * x68));
{  uint128_t x119 = (x110 + ((uint128_t)x112 * x68));
{  uint64_t x120 = (uint64_t) (x116 >> 0x33);
{  uint64_t x121 = ((uint64_t)x116 & 0x7ffffffffffff);
{  uint128_t x122 = (x120 + x117);
{  uint64_t x123 = (uint64_t) (x122 >> 0x33);
{  uint64_t x124 = ((uint64_t)x122 & 0x7ffffffffffff);
{  uint128_t x125 = (x123 + x118);
{  uint64_t x126 = (uint64_t) (x125 >> 0x33);
{  uint64_t x127 = ((uint64_t)x125 & 0x7ffffffffffff);
{  uint128_t x128 = (x126 + x119);
{  uint64_t x129 = (uint64_t) (x128 >> 0x33);
{  uint64_t x130 = ((uint64_t)x128 & 0x7ffffffffffff);
{  uint128_t x131 = (x129 + x111);
{  uint64_t x132 = (uint64_t) (x131 >> 0x33);
{  uint64_t x133 = ((uint64_t)x131 & 0x7ffffffffffff);
{  uint64_t x134 = (x121 + (0x13 * x132));
{  uint64_t x135 = (x134 >> 0x33);
{  uint64_t x136 = (x134 & 0x7ffffffffffff);
{  uint64_t x137 = (x135 + x124);
{  uint64_t x138 = (x137 >> 0x33);
{  uint64_t x139 = (x137 & 0x7ffffffffffff);
{  uint64_t x140 = (x138 + x127);
{  uint64_t x141 = (x99 + x133);
{  uint64_t x142 = (x96 + x130);
{  uint64_t x143 = (x106 + x140);
{  uint64_t x144 = (x105 + x139);
{  uint64_t x145 = (x102 + x136);
{  uint64_t x146 = ((0xffffffffffffe + x99) - x133);
{  uint64_t x147 = ((0xffffffffffffe + x96) - x130);
{  uint64_t x148 = ((0xffffffffffffe + x106) - x140);
{  uint64_t x149 = ((0xffffffffffffe + x105) - x139);
{  uint64_t x150 = ((0xfffffffffffda + x102) - x136);
{  uint64_t x151 = (x145 * 0x2);
{  uint64_t x152 = (x144 * 0x2);
{  uint64_t x153 = ((x143 * 0x2) * 0x13);
{  uint64_t x154 = (x141 * 0x13);
{  uint64_t x155 = (x154 * 0x2);
{  uint128_t x156 = ((((uint128_t)x145 * x145) + ((uint128_t)x155 * x144)) + ((uint128_t)x153 * x142));
{  uint128_t x157 = ((((uint128_t)x151 * x144) + ((uint128_t)x155 * x143)) + ((uint128_t)x142 * (x142 * 0x13)));
{  uint128_t x158 = ((((uint128_t)x151 * x143) + ((uint128_t)x144 * x144)) + ((uint128_t)x155 * x142));
{  uint128_t x159 = ((((uint128_t)x151 * x142) + ((uint128_t)x152 * x143)) + ((uint128_t)x141 * x154));
{  uint128_t x160 = ((((uint128_t)x151 * x141) + ((uint128_t)x152 * x142)) + ((uint128_t)x143 * x143));
{  uint64_t x161 = (uint64_t) (x156 >> 0x33);
{  uint64_t x162 = ((uint64_t)x156 & 0x7ffffffffffff);
{  uint128_t x163 = (x161 + x157);
{  uint64_t x164 = (uint64_t) (x163 >> 0x33);
{  uint64_t x165 = ((uint64_t)x163 & 0x7ffffffffffff);
{  uint128_t x166 = (x164 + x158);
{  uint64_t x167 = (uint64_t) (x166 >> 0x33);
{  uint64_t x168 = ((uint64_t)x166 & 0x7ffffffffffff);
{  uint128_t x169 = (x167 + x159);
{  uint64_t x170 = (uint64_t) (x169 >> 0x33);
{  uint64_t x171 = ((uint64_t)x169 & 0x7ffffffffffff);
{  uint128_t x172 = (x170 + x160);
{  uint64_t x173 = (uint64_t) (x172 >> 0x33);
{  uint64_t x174 = ((uint64_t)x172 & 0x7ffffffffffff);
{  uint64_t x175 = (x162 + (0x13 * x173));
{  uint64_t x176 = (x175 >> 0x33);
{  uint64_t x177 = (x175 & 0x7ffffffffffff);
{  uint64_t x178 = (x176 + x165);
{  uint64_t x179 = (x178 >> 0x33);
{  uint64_t x180 = (x178 & 0x7ffffffffffff);
{  uint64_t x181 = (x179 + x168);
{  uint64_t x182 = (x150 * 0x2);
{  uint64_t x183 = (x149 * 0x2);
{  uint64_t x184 = ((x148 * 0x2) * 0x13);
{  uint64_t x185 = (x146 * 0x13);
{  uint64_t x186 = (x185 * 0x2);
{  uint128_t x187 = ((((uint128_t)x150 * x150) + ((uint128_t)x186 * x149)) + ((uint128_t)x184 * x147));
{  uint128_t x188 = ((((uint128_t)x182 * x149) + ((uint128_t)x186 * x148)) + ((uint128_t)x147 * (x147 * 0x13)));
{  uint128_t x189 = ((((uint128_t)x182 * x148) + ((uint128_t)x149 * x149)) + ((uint128_t)x186 * x147));
{  uint128_t x190 = ((((uint128_t)x182 * x147) + ((uint128_t)x183 * x148)) + ((uint128_t)x146 * x185));
{  uint128_t x191 = ((((uint128_t)x182 * x146) + ((uint128_t)x183 * x147)) + ((uint128_t)x148 * x148));
{  uint64_t x192 = (uint64_t) (x187 >> 0x33);
{  uint64_t x193 = ((uint64_t)x187 & 0x7ffffffffffff);
{  uint128_t x194 = (x192 + x188);
{  uint64_t x195 = (uint64_t) (x194 >> 0x33);
{  uint64_t x196 = ((uint64_t)x194 & 0x7ffffffffffff);
{  uint128_t x197 = (x195 + x189);
{  uint64_t x198 = (uint64_t) (x197 >> 0x33);
{  uint64_t x199 = ((uint64_t)x197 & 0x7ffffffffffff);
{  uint128_t x200 = (x198 + x190);
{  uint64_t x201 = (uint64_t) (x200 >> 0x33);
{  uint64_t x202 = ((uint64_t)x200 & 0x7ffffffffffff);
{  uint128_t x203 = (x201 + x191);
{  uint64_t x204 = (uint64_t) (x203 >> 0x33);
{  uint64_t x205 = ((uint64_t)x203 & 0x7ffffffffffff);
{  uint64_t x206 = (x193 + (0x13 * x204));
{  uint64_t x207 = (x206 >> 0x33);
{  uint64_t x208 = (x206 & 0x7ffffffffffff);
{  uint64_t x209 = (x207 + x196);
{  uint64_t x210 = (x209 >> 0x33);
{  uint64_t x211 = (x209 & 0x7ffffffffffff);
{  uint64_t x212 = (x210 + x199);
{  uint128_t x213 = ((uint128_t)x208 * x10);
{  uint128_t x214 = (((uint128_t)x208 * x12) + ((uint128_t)x211 * x10));
{  uint128_t x215 = ((((uint128_t)x208 * x14) + ((uint128_t)x212 * x10)) + ((uint128_t)x211 * x12));
{  uint128_t x216 = (((((uint128_t)x208 * x16) + ((uint128_t)x202 * x10)) + ((uint128_t)x211 * x14)) + ((uint128_t)x212 * x12));
{  uint128_t x217 = ((((((uint128_t)x208 * x15) + ((uint128_t)x205 * x10)) + ((uint128_t)x202 * x12)) + ((uint128_t)x211 * x16)) + ((uint128_t)x212 * x14));
{  uint64_t x218 = (x205 * 0x13);
{  uint64_t x219 = (x211 * 0x13);
{  uint64_t x220 = (x212 * 0x13);
{  uint64_t x221 = (x202 * 0x13);
{  uint128_t x222 = ((((x213 + ((uint128_t)x218 * x12)) + ((uint128_t)x219 * x15)) + ((uint128_t)x220 * x16)) + ((uint128_t)x221 * x14));
{  uint128_t x223 = (((x214 + ((uint128_t)x218 * x14)) + ((uint128_t)x220 * x15)) + ((uint128_t)x221 * x16));
{  uint128_t x224 = ((x215 + ((uint128_t)x218 * x16)) + ((uint128_t)x221 * x15));
{  uint128_t x225 = (x216 + ((uint128_t)x218 * x15));
{  uint64_t x226 = (uint64_t) (x222 >> 0x33);
{  uint64_t x227 = ((uint64_t)x222 & 0x7ffffffffffff);
{  uint128_t x228 = (x226 + x223);
{  uint64_t x229 = (uint64_t) (x228 >> 0x33);
{  uint64_t x230 = ((uint64_t)x228 & 0x7ffffffffffff);
{  uint128_t x231 = (x229 + x224);
{  uint64_t x232 = (uint64_t) (x231 >> 0x33);
{  uint64_t x233 = ((uint64_t)x231 & 0x7ffffffffffff);
{  uint128_t x234 = (x232 + x225);
{  uint64_t x235 = (uint64_t) (x234 >> 0x33);
{  uint64_t x236 = ((uint64_t)x234 & 0x7ffffffffffff);
{  uint128_t x237 = (x235 + x217);
{  uint64_t x238 = (uint64_t) (x237 >> 0x33);
{  uint64_t x239 = ((uint64_t)x237 & 0x7ffffffffffff);
{  uint64_t x240 = (x227 + (0x13 * x238));
{  uint64_t x241 = (x240 >> 0x33);
{  uint64_t x242 = (x240 & 0x7ffffffffffff);
{  uint64_t x243 = (x241 + x230);
{  uint64_t x244 = (x243 >> 0x33);
{  uint64_t x245 = (x243 & 0x7ffffffffffff);
{  uint64_t x246 = (x244 + x233);
{  uint64_t x247 = (x57 * 0x2);
{  uint64_t x248 = (x56 * 0x2);
{  uint64_t x249 = ((x55 * 0x2) * 0x13);
{  uint64_t x250 = (x53 * 0x13);
{  uint64_t x251 = (x250 * 0x2);
{  uint128_t x252 = ((((uint128_t)x57 * x57) + ((uint128_t)x251 * x56)) + ((uint128_t)x249 * x54));
{  uint128_t x253 = ((((uint128_t)x247 * x56) + ((uint128_t)x251 * x55)) + ((uint128_t)x54 * (x54 * 0x13)));
{  uint128_t x254 = ((((uint128_t)x247 * x55) + ((uint128_t)x56 * x56)) + ((uint128_t)x251 * x54));
{  uint128_t x255 = ((((uint128_t)x247 * x54) + ((uint128_t)x248 * x55)) + ((uint128_t)x53 * x250));
{  uint128_t x256 = ((((uint128_t)x247 * x53) + ((uint128_t)x248 * x54)) + ((uint128_t)x55 * x55));
{  uint64_t x257 = (uint64_t) (x252 >> 0x33);
{  uint64_t x258 = ((uint64_t)x252 & 0x7ffffffffffff);
{  uint128_t x259 = (x257 + x253);
{  uint64_t x260 = (uint64_t) (x259 >> 0x33);
{  uint64_t x261 = ((uint64_t)x259 & 0x7ffffffffffff);
{  uint128_t x262 = (x260 + x254);
{  uint64_t x263 = (uint64_t) (x262 >> 0x33);
{  uint64_t x264 = ((uint64_t)x262 & 0x7ffffffffffff);
{  uint128_t x265 = (x263 + x255);
{  uint64_t x266 = (uint64_t) (x265 >> 0x33);
{  uint64_t x267 = ((uint64_t)x265 & 0x7ffffffffffff);
{  uint128_t x268 = (x266 + x256);
{  uint64_t x269 = (uint64_t) (x268 >> 0x33);
{  uint64_t x270 = ((uint64_t)x268 & 0x7ffffffffffff);
{  uint64_t x271 = (x258 + (0x13 * x269));
{  uint64_t x272 = (x271 >> 0x33);
{  uint64_t x273 = (x271 & 0x7ffffffffffff);
{  uint64_t x274 = (x272 + x261);
{  uint64_t x275 = (x274 >> 0x33);
{  uint64_t x276 = (x274 & 0x7ffffffffffff);
{  uint64_t x277 = (x275 + x264);
{  uint64_t x278 = (x62 * 0x2);
{  uint64_t x279 = (x61 * 0x2);
{  uint64_t x280 = ((x60 * 0x2) * 0x13);
{  uint64_t x281 = (x58 * 0x13);
{  uint64_t x282 = (x281 * 0x2);
{  uint128_t x283 = ((((uint128_t)x62 * x62) + ((uint128_t)x282 * x61)) + ((uint128_t)x280 * x59));
{  uint128_t x284 = ((((uint128_t)x278 * x61) + ((uint128_t)x282 * x60)) + ((uint128_t)x59 * (x59 * 0x13)));
{  uint128_t x285 = ((((uint128_t)x278 * x60) + ((uint128_t)x61 * x61)) + ((uint128_t)x282 * x59));
{  uint128_t x286 = ((((uint128_t)x278 * x59) + ((uint128_t)x279 * x60)) + ((uint128_t)x58 * x281));
{  uint128_t x287 = ((((uint128_t)x278 * x58) + ((uint128_t)x279 * x59)) + ((uint128_t)x60 * x60));
{  uint64_t x288 = (uint64_t) (x283 >> 0x33);
{  uint64_t x289 = ((uint64_t)x283 & 0x7ffffffffffff);
{  uint128_t x290 = (x288 + x284);
{  uint64_t x291 = (uint64_t) (x290 >> 0x33);
{  uint64_t x292 = ((uint64_t)x290 & 0x7ffffffffffff);
{  uint128_t x293 = (x291 + x285);
{  uint64_t x294 = (uint64_t) (x293 >> 0x33);
{  uint64_t x295 = ((uint64_t)x293 & 0x7ffffffffffff);
{  uint128_t x296 = (x294 + x286);
{  uint64_t x297 = (uint64_t) (x296 >> 0x33);
{  uint64_t x298 = ((uint64_t)x296 & 0x7ffffffffffff);
{  uint128_t x299 = (x297 + x287);
{  uint64_t x300 = (uint64_t) (x299 >> 0x33);
{  uint64_t x301 = ((uint64_t)x299 & 0x7ffffffffffff);
{  uint64_t x302 = (x289 + (0x13 * x300));
{  uint64_t x303 = (x302 >> 0x33);
{  uint64_t x304 = (x302 & 0x7ffffffffffff);
{  uint64_t x305 = (x303 + x292);
{  uint64_t x306 = (x305 >> 0x33);
{  uint64_t x307 = (x305 & 0x7ffffffffffff);
{  uint64_t x308 = (x306 + x295);
{  uint128_t x309 = ((uint128_t)x273 * x304);
{  uint128_t x310 = (((uint128_t)x273 * x307) + ((uint128_t)x276 * x304));
{  uint128_t x311 = ((((uint128_t)x273 * x308) + ((uint128_t)x277 * x304)) + ((uint128_t)x276 * x307));
{  uint128_t x312 = (((((uint128_t)x273 * x298) + ((uint128_t)x267 * x304)) + ((uint128_t)x276 * x308)) + ((uint128_t)x277 * x307));
{  uint128_t x313 = ((((((uint128_t)x273 * x301) + ((uint128_t)x270 * x304)) + ((uint128_t)x267 * x307)) + ((uint128_t)x276 * x298)) + ((uint128_t)x277 * x308));
{  uint64_t x314 = (x270 * 0x13);
{  uint64_t x315 = (x276 * 0x13);
{  uint64_t x316 = (x277 * 0x13);
{  uint64_t x317 = (x267 * 0x13);
{  uint128_t x318 = ((((x309 + ((uint128_t)x314 * x307)) + ((uint128_t)x315 * x301)) + ((uint128_t)x316 * x298)) + ((uint128_t)x317 * x308));
{  uint128_t x319 = (((x310 + ((uint128_t)x314 * x308)) + ((uint128_t)x316 * x301)) + ((uint128_t)x317 * x298));
{  uint128_t x320 = ((x311 + ((uint128_t)x314 * x298)) + ((uint128_t)x317 * x301));
{  uint128_t x321 = (x312 + ((uint128_t)x314 * x301));
{  uint64_t x322 = (uint64_t) (x318 >> 0x33);
{  uint64_t x323 = ((uint64_t)x318 & 0x7ffffffffffff);
{  uint128_t x324 = (x322 + x319);
{  uint64_t x325 = (uint64_t) (x324 >> 0x33);
{  uint64_t x326 = ((uint64_t)x324 & 0x7ffffffffffff);
{  uint128_t x327 = (x325 + x320);
{  uint64_t x328 = (uint64_t) (x327 >> 0x33);
{  uint64_t x329 = ((uint64_t)x327 & 0x7ffffffffffff);
{  uint128_t x330 = (x328 + x321);
{  uint64_t x331 = (uint64_t) (x330 >> 0x33);
{  uint64_t x332 = ((uint64_t)x330 & 0x7ffffffffffff);
{  uint128_t x333 = (x331 + x313);
{  uint64_t x334 = (uint64_t) (x333 >> 0x33);
{  uint64_t x335 = ((uint64_t)x333 & 0x7ffffffffffff);
{  uint64_t x336 = (x323 + (0x13 * x334));
{  uint64_t x337 = (x336 >> 0x33);
{  uint64_t x338 = (x336 & 0x7ffffffffffff);
{  uint64_t x339 = (x337 + x326);
{  uint64_t x340 = (x339 >> 0x33);
{  uint64_t x341 = (x339 & 0x7ffffffffffff);
{  uint64_t x342 = (x340 + x329);
{  uint64_t x343 = ((0xffffffffffffe + x270) - x301);
{  uint64_t x344 = ((0xffffffffffffe + x267) - x298);
{  uint64_t x345 = ((0xffffffffffffe + x277) - x308);
{  uint64_t x346 = ((0xffffffffffffe + x276) - x307);
{  uint64_t x347 = ((0xfffffffffffda + x273) - x304);
{  uint128_t x348 = ((uint128_t)x347 * 0x1db41);
{  uint128_t x349 = ((uint128_t)x346 * 0x1db41);
{  uint128_t x350 = ((uint128_t)x345 * 0x1db41);
{  uint128_t x351 = ((uint128_t)x344 * 0x1db41);
{  uint128_t x352 = ((uint128_t)x343 * 0x1db41);
{  uint64_t x353 = (uint64_t) (x348 >> 0x33);
{  uint64_t x354 = ((uint64_t)x348 & 0x7ffffffffffff);
{  uint128_t x355 = (x353 + x349);
{  uint64_t x356 = (uint64_t) (x355 >> 0x33);
{  uint64_t x357 = ((uint64_t)x355 & 0x7ffffffffffff);
{  uint128_t x358 = (x356 + x350);
{  uint64_t x359 = (uint64_t) (x358 >> 0x33);
{  uint64_t x360 = ((uint64_t)x358 & 0x7ffffffffffff);
{  uint128_t x361 = (x359 + x351);
{  uint64_t x362 = (uint64_t) (x361 >> 0x33);
{  uint64_t x363 = ((uint64_t)x361 & 0x7ffffffffffff);
{  uint128_t x364 = (x362 + x352);
{  uint64_t x365 = (uint64_t) (x364 >> 0x33);
{  uint64_t x366 = ((uint64_t)x364 & 0x7ffffffffffff);
{  uint64_t x367 = (x354 + (0x13 * x365));
{  uint64_t x368 = (x367 >> 0x33);
{  uint64_t x369 = (x367 & 0x7ffffffffffff);
{  uint64_t x370 = (x368 + x357);
{  uint64_t x371 = (x370 >> 0x33);
{  uint64_t x372 = (x370 & 0x7ffffffffffff);
{  uint64_t x373 = (x371 + x360);
{  uint64_t x374 = (x366 + x270);
{  uint64_t x375 = (x363 + x267);
{  uint64_t x376 = (x373 + x277);
{  uint64_t x377 = (x372 + x276);
{  uint64_t x378 = (x369 + x273);
{  uint128_t x379 = ((uint128_t)x347 * x378);
{  uint128_t x380 = (((uint128_t)x347 * x377) + ((uint128_t)x346 * x378));
{  uint128_t x381 = ((((uint128_t)x347 * x376) + ((uint128_t)x345 * x378)) + ((uint128_t)x346 * x377));
{  uint128_t x382 = (((((uint128_t)x347 * x375) + ((uint128_t)x344 * x378)) + ((uint128_t)x346 * x376)) + ((uint128_t)x345 * x377));
{  uint128_t x383 = ((((((uint128_t)x347 * x374) + ((uint128_t)x343 * x378)) + ((uint128_t)x344 * x377)) + ((uint128_t)x346 * x375)) + ((uint128_t)x345 * x376));
{  uint64_t x384 = (x343 * 0x13);
{  uint64_t x385 = (x346 * 0x13);
{  uint64_t x386 = (x345 * 0x13);
{  uint64_t x387 = (x344 * 0x13);
{  uint128_t x388 = ((((x379 + ((uint128_t)x384 * x377)) + ((uint128_t)x385 * x374)) + ((uint128_t)x386 * x375)) + ((uint128_t)x387 * x376));
{  uint128_t x389 = (((x380 + ((uint128_t)x384 * x376)) + ((uint128_t)x386 * x374)) + ((uint128_t)x387 * x375));
{  uint128_t x390 = ((x381 + ((uint128_t)x384 * x375)) + ((uint128_t)x387 * x374));
{  uint128_t x391 = (x382 + ((uint128_t)x384 * x374));
{  uint64_t x392 = (uint64_t) (x388 >> 0x33);
{  uint64_t x393 = ((uint64_t)x388 & 0x7ffffffffffff);
{  uint128_t x394 = (x392 + x389);
{  uint64_t x395 = (uint64_t) (x394 >> 0x33);
{  uint64_t x396 = ((uint64_t)x394 & 0x7ffffffffffff);
{  uint128_t x397 = (x395 + x390);
{  uint64_t x398 = (uint64_t) (x397 >> 0x33);
{  uint64_t x399 = ((uint64_t)x397 & 0x7ffffffffffff);
{  uint128_t x400 = (x398 + x391);
{  uint64_t x401 = (uint64_t) (x400 >> 0x33);
{  uint64_t x402 = ((uint64_t)x400 & 0x7ffffffffffff);
{  uint128_t x403 = (x401 + x383);
{  uint64_t x404 = (uint64_t) (x403 >> 0x33);
{  uint64_t x405 = ((uint64_t)x403 & 0x7ffffffffffff);
{  uint64_t x406 = (x393 + (0x13 * x404));
{  uint64_t x407 = (x406 >> 0x33);
{  uint64_t x408 = (x406 & 0x7ffffffffffff);
{  uint64_t x409 = (x407 + x396);
{  uint64_t x410 = (x409 >> 0x33);
{  uint64_t x411 = (x409 & 0x7ffffffffffff);
{  uint64_t x412 = (x410 + x399);
out[0] = x335;
out[1] = x332;
out[2] = x342;
out[3] = x341;
out[4] = x338;
out[5] = x405;
out[6] = x402;
out[7] = x412;
out[8] = x411;
out[9] = x408;
out[10] = x174;
out[11] = x171;
out[12] = x181;
out[13] = x180;
out[14] = x177;
out[15] = x239;
out[16] = x236;
out[17] = x246;
out[18] = x245;
out[19] = x242;
}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
// caller: uint64_t out[20];
